CHOICE-STRATEGY-IS: 
ANCESTRY∧SUPPORT[THEOREM]∧EQUALITY[=,4];

EDIT-STRATEGY-IS: 
α(C)>1∨∂(C)>3;

ELAPSED-TIME =2150

NIL 1 2
1 (x ⊗(y ⊗ z))=(z ⊗(y ⊗ x));G3
2 ¬((THEOREM2 ⊗ THEOREM1)⊗(THEOREM3 ⊗ THEOREM1))=(THEOREM2 ⊗ THEOREM3);THEOREM